(set-logic ALL)
(set-info :status unsat)
(declare-sort $$unsorted 0)
(declare-fun tptp.skc17 () $$unsorted)
(declare-fun tptp.actual_world ($$unsorted) Bool)
(assert (tptp.actual_world tptp.skc17))
(declare-fun tptp.skc11 () $$unsorted)
(assert (tptp.actual_world tptp.skc11))
(declare-fun tptp.ssSkC0 () Bool)
(declare-fun tptp.skc20 () $$unsorted)
(declare-fun tptp.city ($$unsorted $$unsorted) Bool)
(assert (or tptp.ssSkC0 (tptp.city tptp.skc17 tptp.skc20)))
(declare-fun tptp.street ($$unsorted $$unsorted) Bool)
(assert (or tptp.ssSkC0 (tptp.street tptp.skc17 tptp.skc20)))
(declare-fun tptp.lonely ($$unsorted $$unsorted) Bool)
(assert (or tptp.ssSkC0 (tptp.lonely tptp.skc17 tptp.skc20)))
(declare-fun tptp.skc21 () $$unsorted)
(declare-fun tptp.placename ($$unsorted $$unsorted) Bool)
(assert (or tptp.ssSkC0 (tptp.placename tptp.skc17 tptp.skc21)))
(declare-fun tptp.hollywood_placename ($$unsorted $$unsorted) Bool)
(assert (or tptp.ssSkC0 (tptp.hollywood_placename tptp.skc17 tptp.skc21)))
(declare-fun tptp.skc18 () $$unsorted)
(declare-fun tptp.event ($$unsorted $$unsorted) Bool)
(assert (or tptp.ssSkC0 (tptp.event tptp.skc17 tptp.skc18)))
(declare-fun tptp.present ($$unsorted $$unsorted) Bool)
(assert (or tptp.ssSkC0 (tptp.present tptp.skc17 tptp.skc18)))
(declare-fun tptp.barrel ($$unsorted $$unsorted) Bool)
(assert (or tptp.ssSkC0 (tptp.barrel tptp.skc17 tptp.skc18)))
(declare-fun tptp.skc19 () $$unsorted)
(declare-fun tptp.old ($$unsorted $$unsorted) Bool)
(assert (or tptp.ssSkC0 (tptp.old tptp.skc17 tptp.skc19)))
(declare-fun tptp.dirty ($$unsorted $$unsorted) Bool)
(assert (or tptp.ssSkC0 (tptp.dirty tptp.skc17 tptp.skc19)))
(declare-fun tptp.white ($$unsorted $$unsorted) Bool)
(assert (or tptp.ssSkC0 (tptp.white tptp.skc17 tptp.skc19)))
(declare-fun tptp.chevy ($$unsorted $$unsorted) Bool)
(assert (or tptp.ssSkC0 (tptp.chevy tptp.skc17 tptp.skc19)))
(declare-fun tptp.skc16 () $$unsorted)
(assert (or (not tptp.ssSkC0) (tptp.lonely tptp.skc11 tptp.skc16)))
(assert (or (not tptp.ssSkC0) (tptp.street tptp.skc11 tptp.skc16)))
(declare-fun tptp.skc12 () $$unsorted)
(assert (or (not tptp.ssSkC0) (tptp.barrel tptp.skc11 tptp.skc12)))
(assert (or (not tptp.ssSkC0) (tptp.present tptp.skc11 tptp.skc12)))
(assert (or (not tptp.ssSkC0) (tptp.event tptp.skc11 tptp.skc12)))
(declare-fun tptp.skc14 () $$unsorted)
(assert (or (not tptp.ssSkC0) (tptp.hollywood_placename tptp.skc11 tptp.skc14)))
(assert (or (not tptp.ssSkC0) (tptp.placename tptp.skc11 tptp.skc14)))
(declare-fun tptp.skc15 () $$unsorted)
(assert (or (not tptp.ssSkC0) (tptp.city tptp.skc11 tptp.skc15)))
(declare-fun tptp.skc13 () $$unsorted)
(assert (or (not tptp.ssSkC0) (tptp.chevy tptp.skc11 tptp.skc13)))
(assert (or (not tptp.ssSkC0) (tptp.white tptp.skc11 tptp.skc13)))
(assert (or (not tptp.ssSkC0) (tptp.dirty tptp.skc11 tptp.skc13)))
(assert (or (not tptp.ssSkC0) (tptp.old tptp.skc11 tptp.skc13)))
(declare-fun tptp.down ($$unsorted $$unsorted $$unsorted) Bool)
(assert (or tptp.ssSkC0 (tptp.down tptp.skc17 tptp.skc18 tptp.skc20)))
(declare-fun tptp.in ($$unsorted $$unsorted $$unsorted) Bool)
(assert (or tptp.ssSkC0 (tptp.in tptp.skc17 tptp.skc18 tptp.skc20)))
(declare-fun tptp.of ($$unsorted $$unsorted $$unsorted) Bool)
(assert (or tptp.ssSkC0 (tptp.of tptp.skc17 tptp.skc21 tptp.skc20)))
(declare-fun tptp.agent ($$unsorted $$unsorted $$unsorted) Bool)
(assert (or tptp.ssSkC0 (tptp.agent tptp.skc17 tptp.skc18 tptp.skc19)))
(assert (or (not tptp.ssSkC0) (tptp.down tptp.skc11 tptp.skc12 tptp.skc16)))
(assert (or (not tptp.ssSkC0) (tptp.in tptp.skc11 tptp.skc12 tptp.skc15)))
(assert (or (not tptp.ssSkC0) (tptp.of tptp.skc11 tptp.skc14 tptp.skc15)))
(assert (or (not tptp.ssSkC0) (tptp.agent tptp.skc11 tptp.skc12 tptp.skc13)))
(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted)) (or (not (tptp.down U V W)) (not (tptp.lonely U W)) (not (tptp.street U W)) (not (tptp.barrel U V)) (not (tptp.present U V)) (not (tptp.event U V)) (not (tptp.hollywood_placename U X)) (not (tptp.placename U X)) (not (tptp.in U V Y)) (not (tptp.city U Y)) (not (tptp.of U X Y)) (not (tptp.chevy U Z)) (not (tptp.white U Z)) (not (tptp.dirty U Z)) (not (tptp.old U Z)) (not (tptp.agent U V Z)) (not (tptp.actual_world U)) tptp.ssSkC0)))
(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted)) (or (not (tptp.city U V)) (not (tptp.street U V)) (not (tptp.lonely U V)) (not (tptp.down U W V)) (not (tptp.in U W V)) (not (tptp.placename U X)) (not (tptp.hollywood_placename U X)) (not (tptp.of U X V)) (not (tptp.event U W)) (not (tptp.present U W)) (not (tptp.barrel U W)) (not (tptp.agent U W Y)) (not (tptp.old U Y)) (not (tptp.dirty U Y)) (not (tptp.white U Y)) (not (tptp.chevy U Y)) (not (tptp.actual_world U)) (not tptp.ssSkC0))))
(set-info :filename NLP114-1)
(check-sat)
